Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

a(s(x1)) → s(a(x1))
b(a(b(s(x1)))) → a(b(s(a(x1))))
b(a(b(b(x1)))) → a(b(a(b(x1))))
a(b(a(a(x1)))) → b(a(b(a(x1))))

Q is empty.


QTRS
  ↳ QTRS Reverse
  ↳ RRRPoloQTRSProof
  ↳ QTRS Reverse

Q restricted rewrite system:
The TRS R consists of the following rules:

a(s(x1)) → s(a(x1))
b(a(b(s(x1)))) → a(b(s(a(x1))))
b(a(b(b(x1)))) → a(b(a(b(x1))))
a(b(a(a(x1)))) → b(a(b(a(x1))))

Q is empty.

We have reversed the following QTRS:
The set of rules R is

a(s(x1)) → s(a(x1))
b(a(b(s(x1)))) → a(b(s(a(x1))))
b(a(b(b(x1)))) → a(b(a(b(x1))))
a(b(a(a(x1)))) → b(a(b(a(x1))))

The set Q is empty.
We have obtained the following QTRS:

s(a(x)) → a(s(x))
s(b(a(b(x)))) → a(s(b(a(x))))
b(b(a(b(x)))) → b(a(b(a(x))))
a(a(b(a(x)))) → a(b(a(b(x))))

The set Q is empty.

↳ QTRS
  ↳ QTRS Reverse
QTRS
  ↳ RRRPoloQTRSProof
  ↳ QTRS Reverse

Q restricted rewrite system:
The TRS R consists of the following rules:

s(a(x)) → a(s(x))
s(b(a(b(x)))) → a(s(b(a(x))))
b(b(a(b(x)))) → b(a(b(a(x))))
a(a(b(a(x)))) → a(b(a(b(x))))

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

a(s(x1)) → s(a(x1))
b(a(b(s(x1)))) → a(b(s(a(x1))))
b(a(b(b(x1)))) → a(b(a(b(x1))))
a(b(a(a(x1)))) → b(a(b(a(x1))))

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

a(s(x1)) → s(a(x1))
b(a(b(s(x1)))) → a(b(s(a(x1))))
Used ordering:
Polynomial interpretation [25]:

POL(a(x1)) = 2·x1   
POL(b(x1)) = 2·x1   
POL(s(x1)) = 2 + 2·x1   




↳ QTRS
  ↳ QTRS Reverse
  ↳ RRRPoloQTRSProof
QTRS
      ↳ DependencyPairsProof
  ↳ QTRS Reverse

Q restricted rewrite system:
The TRS R consists of the following rules:

b(a(b(b(x1)))) → a(b(a(b(x1))))
a(b(a(a(x1)))) → b(a(b(a(x1))))

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

A(b(a(a(x1)))) → B(a(x1))
A(b(a(a(x1)))) → A(b(a(x1)))
B(a(b(b(x1)))) → A(b(x1))
A(b(a(a(x1)))) → B(a(b(a(x1))))
B(a(b(b(x1)))) → B(a(b(x1)))
B(a(b(b(x1)))) → A(b(a(b(x1))))

The TRS R consists of the following rules:

b(a(b(b(x1)))) → a(b(a(b(x1))))
a(b(a(a(x1)))) → b(a(b(a(x1))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS
  ↳ QTRS Reverse
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ DependencyPairsProof
QDP
          ↳ RuleRemovalProof
  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

A(b(a(a(x1)))) → B(a(x1))
A(b(a(a(x1)))) → A(b(a(x1)))
B(a(b(b(x1)))) → A(b(x1))
A(b(a(a(x1)))) → B(a(b(a(x1))))
B(a(b(b(x1)))) → B(a(b(x1)))
B(a(b(b(x1)))) → A(b(a(b(x1))))

The TRS R consists of the following rules:

b(a(b(b(x1)))) → a(b(a(b(x1))))
a(b(a(a(x1)))) → b(a(b(a(x1))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

A(b(a(a(x1)))) → B(a(x1))
A(b(a(a(x1)))) → A(b(a(x1)))
B(a(b(b(x1)))) → A(b(x1))
B(a(b(b(x1)))) → B(a(b(x1)))


Used ordering: POLO with Polynomial interpretation [25]:

POL(A(x1)) = x1   
POL(B(x1)) = x1   
POL(a(x1)) = 2 + 2·x1   
POL(b(x1)) = 2 + 2·x1   



↳ QTRS
  ↳ QTRS Reverse
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ RuleRemovalProof
QDP
              ↳ Narrowing
  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

A(b(a(a(x1)))) → B(a(b(a(x1))))
B(a(b(b(x1)))) → A(b(a(b(x1))))

The TRS R consists of the following rules:

b(a(b(b(x1)))) → a(b(a(b(x1))))
a(b(a(a(x1)))) → b(a(b(a(x1))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule A(b(a(a(x1)))) → B(a(b(a(x1)))) at position [0] we obtained the following new rules:

A(b(a(a(b(a(a(x0))))))) → B(a(b(b(a(b(a(x0)))))))
A(b(a(a(a(x0))))) → B(b(a(b(a(x0)))))
A(b(a(a(b(b(x0)))))) → B(a(a(b(a(b(x0))))))



↳ QTRS
  ↳ QTRS Reverse
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ RuleRemovalProof
            ↳ QDP
              ↳ Narrowing
QDP
                  ↳ Narrowing
  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

A(b(a(a(a(x0))))) → B(b(a(b(a(x0)))))
A(b(a(a(b(a(a(x0))))))) → B(a(b(b(a(b(a(x0)))))))
A(b(a(a(b(b(x0)))))) → B(a(a(b(a(b(x0))))))
B(a(b(b(x1)))) → A(b(a(b(x1))))

The TRS R consists of the following rules:

b(a(b(b(x1)))) → a(b(a(b(x1))))
a(b(a(a(x1)))) → b(a(b(a(x1))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule B(a(b(b(x1)))) → A(b(a(b(x1)))) at position [0] we obtained the following new rules:

B(a(b(b(a(b(b(x0))))))) → A(b(a(a(b(a(b(x0)))))))
B(a(b(b(a(a(x0)))))) → A(b(b(a(b(a(x0))))))
B(a(b(b(b(x0))))) → A(a(b(a(b(x0)))))



↳ QTRS
  ↳ QTRS Reverse
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ RuleRemovalProof
            ↳ QDP
              ↳ Narrowing
                ↳ QDP
                  ↳ Narrowing
QDP
                      ↳ QDPToSRSProof
  ↳ QTRS Reverse

Q DP problem:
The TRS P consists of the following rules:

B(a(b(b(a(b(b(x0))))))) → A(b(a(a(b(a(b(x0)))))))
A(b(a(a(b(a(a(x0))))))) → B(a(b(b(a(b(a(x0)))))))
A(b(a(a(a(x0))))) → B(b(a(b(a(x0)))))
A(b(a(a(b(b(x0)))))) → B(a(a(b(a(b(x0))))))
B(a(b(b(a(a(x0)))))) → A(b(b(a(b(a(x0))))))
B(a(b(b(b(x0))))) → A(a(b(a(b(x0)))))

The TRS R consists of the following rules:

b(a(b(b(x1)))) → a(b(a(b(x1))))
a(b(a(a(x1)))) → b(a(b(a(x1))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The finiteness of this DP problem is implied by strong termination of a SRS due to [12].


↳ QTRS
  ↳ QTRS Reverse
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ RuleRemovalProof
            ↳ QDP
              ↳ Narrowing
                ↳ QDP
                  ↳ Narrowing
                    ↳ QDP
                      ↳ QDPToSRSProof
QTRS
                          ↳ QTRS Reverse
  ↳ QTRS Reverse

Q restricted rewrite system:
The TRS R consists of the following rules:

b(a(b(b(x1)))) → a(b(a(b(x1))))
a(b(a(a(x1)))) → b(a(b(a(x1))))
B(a(b(b(a(b(b(x0))))))) → A(b(a(a(b(a(b(x0)))))))
A(b(a(a(b(a(a(x0))))))) → B(a(b(b(a(b(a(x0)))))))
A(b(a(a(a(x0))))) → B(b(a(b(a(x0)))))
A(b(a(a(b(b(x0)))))) → B(a(a(b(a(b(x0))))))
B(a(b(b(a(a(x0)))))) → A(b(b(a(b(a(x0))))))
B(a(b(b(b(x0))))) → A(a(b(a(b(x0)))))

Q is empty.

We have reversed the following QTRS:
The set of rules R is

b(a(b(b(x1)))) → a(b(a(b(x1))))
a(b(a(a(x1)))) → b(a(b(a(x1))))
B(a(b(b(a(b(b(x0))))))) → A(b(a(a(b(a(b(x0)))))))
A(b(a(a(b(a(a(x0))))))) → B(a(b(b(a(b(a(x0)))))))
A(b(a(a(a(x0))))) → B(b(a(b(a(x0)))))
A(b(a(a(b(b(x0)))))) → B(a(a(b(a(b(x0))))))
B(a(b(b(a(a(x0)))))) → A(b(b(a(b(a(x0))))))
B(a(b(b(b(x0))))) → A(a(b(a(b(x0)))))

The set Q is empty.
We have obtained the following QTRS:

b(b(a(b(x)))) → b(a(b(a(x))))
a(a(b(a(x)))) → a(b(a(b(x))))
b(b(a(b(b(a(B(x))))))) → b(a(b(a(a(b(A(x)))))))
a(a(b(a(a(b(A(x))))))) → a(b(a(b(b(a(B(x)))))))
a(a(a(b(A(x))))) → a(b(a(b(B(x)))))
b(b(a(a(b(A(x)))))) → b(a(b(a(a(B(x))))))
a(a(b(b(a(B(x)))))) → a(b(a(b(b(A(x))))))
b(b(b(a(B(x))))) → b(a(b(a(A(x)))))

The set Q is empty.

↳ QTRS
  ↳ QTRS Reverse
  ↳ RRRPoloQTRSProof
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ RuleRemovalProof
            ↳ QDP
              ↳ Narrowing
                ↳ QDP
                  ↳ Narrowing
                    ↳ QDP
                      ↳ QDPToSRSProof
                        ↳ QTRS
                          ↳ QTRS Reverse
QTRS
                              ↳ RFCMatchBoundsTRSProof
  ↳ QTRS Reverse

Q restricted rewrite system:
The TRS R consists of the following rules:

b(b(a(b(x)))) → b(a(b(a(x))))
a(a(b(a(x)))) → a(b(a(b(x))))
b(b(a(b(b(a(B(x))))))) → b(a(b(a(a(b(A(x)))))))
a(a(b(a(a(b(A(x))))))) → a(b(a(b(b(a(B(x)))))))
a(a(a(b(A(x))))) → a(b(a(b(B(x)))))
b(b(a(a(b(A(x)))))) → b(a(b(a(a(B(x))))))
a(a(b(b(a(B(x)))))) → a(b(a(b(b(A(x))))))
b(b(b(a(B(x))))) → b(a(b(a(A(x)))))

Q is empty.

Termination of the TRS R could be shown with a Match Bound [6,7] of 1. This implies Q-termination of R.
The following rules were used to construct the certificate:

b(b(a(b(x)))) → b(a(b(a(x))))
a(a(b(a(x)))) → a(b(a(b(x))))
b(b(a(b(b(a(B(x))))))) → b(a(b(a(a(b(A(x)))))))
a(a(b(a(a(b(A(x))))))) → a(b(a(b(b(a(B(x)))))))
a(a(a(b(A(x))))) → a(b(a(b(B(x)))))
b(b(a(a(b(A(x)))))) → b(a(b(a(a(B(x))))))
a(a(b(b(a(B(x)))))) → a(b(a(b(b(A(x))))))
b(b(b(a(B(x))))) → b(a(b(a(A(x)))))

The certificate found is represented by the following graph.

The certificate consists of the following enumerated nodes:

507, 508, 511, 512, 510, 509, 514, 515, 513, 517, 516, 522, 523, 519, 520, 518, 521, 527, 528, 526, 524, 525, 529, 531, 532, 530, 533, 534, 540, 539, 536, 537, 535, 538, 543, 544, 541, 542, 548, 549, 547, 545, 546, 550

Node 507 is start node and node 508 is final node.

Those nodes are connect through the following edges:



We have reversed the following QTRS:
The set of rules R is

a(s(x1)) → s(a(x1))
b(a(b(s(x1)))) → a(b(s(a(x1))))
b(a(b(b(x1)))) → a(b(a(b(x1))))
a(b(a(a(x1)))) → b(a(b(a(x1))))

The set Q is empty.
We have obtained the following QTRS:

s(a(x)) → a(s(x))
s(b(a(b(x)))) → a(s(b(a(x))))
b(b(a(b(x)))) → b(a(b(a(x))))
a(a(b(a(x)))) → a(b(a(b(x))))

The set Q is empty.

↳ QTRS
  ↳ QTRS Reverse
  ↳ RRRPoloQTRSProof
  ↳ QTRS Reverse
QTRS

Q restricted rewrite system:
The TRS R consists of the following rules:

s(a(x)) → a(s(x))
s(b(a(b(x)))) → a(s(b(a(x))))
b(b(a(b(x)))) → b(a(b(a(x))))
a(a(b(a(x)))) → a(b(a(b(x))))

Q is empty.